MCE annotation#724
Conversation
…ingsDuringVerification message in some places since it fits better
| case Seq("0") | Seq("greedy") => | ||
| if (Verifier.config.counterexample.isSupplied) | ||
| reporter report AnnotationWarning(s"Member ${member.name} has exhaleMode annotation that may interfere with counterexample generation.") | ||
| false | ||
| case Seq("1") | Seq("mce") | Seq("moreCompleteExhale") => true |
There was a problem hiding this comment.
Does this mean that we wouldn't be able to annotate Viper to use moreCompleteExhale on demand for a method?
There was a problem hiding this comment.
Right. Basically, MCE on demand is a global setting; if that's set, Silicon will always switch to MCE on retry. This annotation sets the default for the given method.
I could change that though.
There was a problem hiding this comment.
In the router package in SCION, I have an example where I want the package to be verified with mce, except for a particular method where mceOnDemand is useful. With the current approach, I would need to set-up the mode as mce on demand and potentially have to annotate almost all methods with mce (which is fine, only a bit verbose). If adding the option for mce on demand requires only small changes to silicon, I would be grateful for that feature. Otherwise, I wouldn't bother changing it.
| false | ||
| case Seq("1") | Seq("mce") | Seq("moreCompleteExhale") => true | ||
| case v => | ||
| reporter report AnnotationWarning(s"Member ${member.name} has invalid exhaleMode annotation value $v. Annotation will be ignored.") |
There was a problem hiding this comment.
I would reject this one via a consistency check instead of reporting a warning (I think it might be very easy for a front-end developer to miss the warning otherwise)
There was a problem hiding this comment.
Mh I'm not sure. A consistency check is an AST-level check that's usually independent of the backend, right, and this is a backend-specific annotation. So we'd either need to build in checks regarding what a correct annotation is right into the AnnotationInfo AST node, which seems wrong to me, since annotations should in principle allow you to add all kinds of stuff in a flexible way. Or it wouldn't be a consistency check and we'd return an AnnotationError here instead, so you wouldn't be able to ignore it.
This might actually be something we should discuss with more people, since this will come up again and again.
There was a problem hiding this comment.
I think you are right about reporting consistency errors for annotations. At first sight, reporting an AnnotationError here instead of AnnotationWarning sounds like the best option.
There was a problem hiding this comment.
Yeah I can see that. Actually the more I think about it the more a backend-specific consistency check would also make sense. But I think this is just something we need to discuss and decide once and for all, for annotations in general. I think it's not super clear what's best. IMO warnings could also make sense:
- We at some point had the idea that it should always be sound to ignore an annotation.
- We can't reliably flag errors for all potential problems here. E.g. we would detect
@exhaleMode("nce")but not@exhaleNode("mce"). For the latter we can't flag an error (at most a warning), it's just an annotation we don't recognize, and we can't flag errors for all annotations we don't recognize since otherwise Carbon would have to reject all programs with Silicon-specific annotations.
So I'd suggest going with the warning for now and making sure we discuss this asap. Changing this to an error would be super quick and simple of course.
2 participants
Introduces an annotation to set the exhale mode for individual members, i.e., to override the mode set per command line parameter for this member.
The annotation is
@exhaleMode("x"), wherexcan beAll other values (or multiple values) will result in a warning and the default will be used.
There will also be a warning when setting greedy mode per annotation when counterexamples are enables, since counterexamples generally don't work correctly with greedy mode.
Additionally, the PR changes type checker warnings that aren't type checker warnings to use a newly-added warning type (we were misusing type checker warnings previously because there were no verifier warnings).
Depends on a Silver PR that adds two new types of messages and also adds a test for the exhaleMode annotation. This PR must be merged before the quantifier weight annotation PR.